(include-book "../src/acl2/command-handler")
(include-book "generators/world-data-generators")
;;;Tests for the Command Handler System

;;Verify that the play function sets the framerate to
;;"play speed" and otherwise leaves the world unchanged.
(defproperty play-test
    (init :value (random-lifelike-world))
    (let*  ((new (play init)))
        (and (equal (cell-world-grid init) (cell-world-grid new))
             (equal (cell-world-rules init) (cell-world-rules new))
             (equal (cell-world-framerate new) *play-speed*)
             (equal (cell-world-changeset init) 
                                (cell-world-changeset new))
             (equal (cell-world-num-commands-read init) 
                                (cell-world-num-commands-read new))
             (equal (cell-world-gen-num init) 
                                (cell-world-gen-num new)))))

;;Verify that the pause function sets the framerate to
;;0 and otherwise leaves the world unchanged.
(defproperty pause-test
    (init :value (random-lifelike-world))
    (let*  ((new (pause init)))
        (and (equal (cell-world-grid init) (cell-world-grid new))
             (equal (cell-world-rules init) (cell-world-rules new))
             (equal (cell-world-framerate new) 0)
             (equal (cell-world-changeset init) (cell-world-changeset new))
             (equal (cell-world-num-commands-read init) 
                                (cell-world-num-commands-read new))
             (equal (cell-world-gen-num init) 
                                (cell-world-gen-num new)))))
`
;;Verify that the fast-forward function sets the framerate to
;;Fast-forward speed and otherwise leaves the world unchanged.
(defproperty fast-forward-test
    (init :value (random-lifelike-world))
    (let*  ((new (fast-forward init)))
        (and (equal (cell-world-grid init) (cell-world-grid new))
             (equal (cell-world-rules init) (cell-world-rules new))
             (equal (cell-world-framerate new) *ff-speed*)
             (equal (cell-world-changeset init) (cell-world-changeset new))
             (equal (cell-world-num-commands-read init) 
                                (cell-world-num-commands-read new))
             (equal (cell-world-gen-num init) 
                                (cell-world-gen-num new)))))

;;Verify that the set-cell function toggles the given
;;cell and otherwise leaves the world unchanged.
(defproperty set-cell-test
    (init :value (random-lifelike-world)
         x :value (random-integer)
         y :value (random-integer))
    (let*  ((new (set-cell init x y (not (lifelike-grid-get (cell-world-grid init) x y)))))
        (and (not (equal (cell-world-grid init) (cell-world-grid new)))
                     (equal (lifelike-grid-set (cell-world-grid init) x y t) (cell-world-grid new))
                     (equal (cell-world-rules init) (cell-world-rules new))
                     (equal (cell-world-framerate init) (cell-world-framerate new))
                     (equal (cell-world-changeset init) (cell-world-changeset new))
                     (equal (cell-world-num-commands-read init) 
                                (cell-world-num-commands-read new))
                     (equal (cell-world-gen-num init) 
                                (cell-world-gen-num new)))))

